$\forall$$A$, $B$:Type, $a$:EqDecider($A$), $b$:EqDecider($B$). product{-}deq($A$;$B$;$a$;$b$) $\in$ EqDecider($A$$\times$$B$)